Section: New Results

Underapproximation for Precondition Inference

Participants : Patrick Cousot, Radhia Cousot, Francesco Logozzo [Microsoft Research (Redmond, USA)] , Manuel Fähndrichh [Microsoft Research (Redmond, USA)] .

In the context of program design by contracts, programmers often insert assertions in their code to be optionally checked at runtime, at least during the debugging phase. These assertions would better be given as a precondition of the method/procedure in which they appear. Potential errors would be discovered earlier and, more importantly, the precondition could be used in the context of separate static program analysis as part of the abstract semantics of the code. However in the case of collections (data structures such as arrays, lists, etc) checking both the precondition and the assertions at runtime appears superfluous and costly. So the precondition is often omitted since it is checked anyway at runtime by the assertions. It follows that the static analysis can be much less precise, a fact that can be difficult to understand since “the precondition and assertions are equivalent” (i.e. at runtime, up to the time at which warnings are produced, but not statically) e.g. for separate static analysis. Moreover preconditions are often understood as overapproximations and thus may exclude good runs which is counter-intuitive for programmers. On the contrary, with considering underapproximations [37] , [28] which exclude no good run, ensures that if the precondition is violated then a runtime error must definitely be raised later, and if the precondition is not strong enough to catch all errors they will definitely be captures by a later runtime check.

In [19] , we define precisely and formally the contract inference problem from intermittent assertions on scalar variables and elements of collections inserted in the code by the programmer. Our definition excludes no good run even when a non-deterministic choice (e.g. an interactive input) could lead to a bad one. We then introduce new abstract interpretation-based methods to automatically infer both the static contract precondition of a method/procedure and the code to check it at runtime on scalar and collection variables. It has been implemented in CCCheck (formerly Clousot ) by Francesco Logozzo and Manuel Fähndrich.